ds, da, x, T:Top, ks:Top List, tr:Top, j, i:Id.
R-has-loc(R-state-var(i;ds;da;x;T;ks;tr);j) ~ i = j 

latex

Definitions	t  T, x:AB(x), x:A. B(x), es realizer ind Reffect compseq tag def, R-has-loc(R;i), Void, x:A. B(x), Top, x. t(x), es realizer ind Rframe compseq tag def, es realizer ind Rplus compseq tag def, R-state-var(i;ds;da;x;T;ks;tr), type List, Id, false, true, p  q, <a,b>, , s = t, Prop, b, Type, A, b, P  Q, x:AB(x), P & Q, P  Q, Unit, left+right, {T}, SQType(T), s ~ t, a = b
Lemmas	bool sq, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, bnot wf, not wf, assert wf, eq id wf, bool wf, btrue wf, bfalse wf, Id wf, top wf, Rall-has-loc